es:ES, l:IdLnk, tg:Id, A:Type, e:E.
(kindtype(destination(l);rcv(l,tg)) r A)
 ((e  es-in-port(es;l;tg)))
 (es-in-port(es;l;tg)(e) = val(e)  A) 

latex

Definitions	x:A. B(x), P  Q, t  T, b, e  X, es-in-port(es;l;tg), X(e), can-apply(f;x), if b then t else f fi , do-apply(f;x), isl(x), outl(x), , tt, ff, , Top, Id, SQType(T), {T}, P  Q, lnk(e), P  Q, P & Q, False, Unit, A c B,
Lemmas	assert wf, es-kindtype wf, ldst wf, rcv wf, es-E wf, Id wf, IdLnk wf, event system wf, eq knd wf, es-kind wf, bool wf, true wf, bnot wf, not wf, it wf, unit wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, assert-eq-knd, es-valtype-kindtype, Knd sq, Id sq, es-loc wf, es-isrcv-loc, es-kind-rcv, btrue wf, bfalse wf